\begin{tabbing}
$\forall$$k$:Knd, $l$:IdLnk, ${\it ds}$, ${\it dt}$:$x$:Id fp$\rightarrow$ Type, $T$:Type.
\\[0ex](($\uparrow$isrcv($k$))
\\[0ex]$\Rightarrow$ \=(destination(lnk($k$)) = source($l$) $\in$ Id\+
\\[0ex]\& ((lnk($k$) = $l$) $\Rightarrow$ ($T$ = DeclaredType(${\it dt}$;tag($k$))))))
\-\\[0ex]$\Rightarrow$ \=($\forall$$g$:((${\it tg}$:Id $\times$ (State(${\it ds}$)$\rightarrow$$T$$\rightarrow$(DeclaredType(${\it dt}$;${\it tg}$) List))) List).\+
\\[0ex]@source($l$): with declarations 
\\[0ex]ds:${\it ds}$
\\[0ex]d\=a:$k$ : $T$ $\oplus$ lnk{-}decl($l$;${\it dt}$)\+
\\[0ex]$k$(v) sends $g$ s v on link $l$ 
\-\\[0ex]realizes ${\it es}$.
\\[0ex]sends $k$(v:$T$) on $l$:
\\[0ex]tagged($g$,State(${\it ds}$),v):${\it dt}$)
\-
\end{tabbing}